Nuprl Lemma : free-from-atom-outr
11,40
postcript
pdf
A
:Type,
x
:(Top +
A
),
a
:Atom1.
x
:Top +
A
||
a
(
(
isl(
x
)))
outr(
x
):
A
||
a
latex
Definitions
t
T
,
True
,
outr(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
False
,
if
b
then
t
else
f
fi
,
ff
,
tt
,
isl(
x
)
,
b
,
A
Lemmas
top
wf
,
free-from-atom
wf1
,
isl
wf
,
assert
wf
,
not
wf
origin
A:Type, x:(Top + A), a:Atom1. x:Top + A||a 
(
(
isl(x))) outr(x):A||a A:Type, x:(Top + A), a:Atom1. x:Top + A||a ((isl(x))) outr(x):A||a 
T Qx:A. B(x)
bA